Report for doc/examples/arithmetic_2.c

Generated on 2024-08-21 20:22:51 by CPAchecker 3.0 / testCaseGeneration-bmc

Matches in value-assignements (V): {{numOfValueMatches}}

Matches in edge-description: {{numOfDescriptionMatches}}

Rank
Scope
-V-
{{line.bestrank}}
{{line.desc}}
Precondition (initial variable assignment):

{{precondition}}

{{fault.rank}}. {{fault.score}} Details:
Current values:
Name Value
1
//#include <stdio.h>  
2
//#include <stdlib.h>  
3
//#include <assert.h>  
4
  
5
// Structure to hold division result  
6
//typedef struct {  
7
//   int quotient;  
8
//    int remainder;  
9
//} DivisionResult;  
10
  
11
// Function prototypes  
12
  
13
// Arithmetic class implementation  
14
int add(int a, int b) {  
15
    //assert(a >= -100 && a <= 100);  
16
    //assert(b >= -100 && b <= 100);  
17
  
18
    int i, result;  
19
  
20
    if (b >= 0) {  
21
        //printf("branch 2\n");  
22
        result = a;  
23
        i = b;  
24
        while (i != 0) {  
25
            result = result + 1;  
26
            i = i - 1;  
27
        }  
28
    } else {  
29
        //printf("branch 3\n");  
30
        result = a;  
31
        i = b;  
32
        while (i != 0) {  
33
            result = result - 1;  
34
            i = i + 1;  
35
        }  
36
    }  
37
    return result;  
38
}  
39
  
40
int add_recursive(int a, int b) {  
41
    //assert(a >= -100 && a <= 100);  
42
    //assert(b >= -100 && b <= 100);  
43
  
44
    int result;  
45
    if (b == 0) {  
46
        //printf("branch 4\n");  
47
        result = a;  
48
    } else if (b > 0) {  
49
        //printf("branch 5\n");  
50
        result = add_recursive(a, b - 1) + 1;  
51
    } else {  
52
        //printf("branch 6\n");  
53
        result = add_recursive(a, b + 1) - 1;  
54
    }  
55
    return result;  
56
}  
57
  
58
int multiply(int a, int b) {  
59
    //assert(a >= -10 && a <= 10);  
60
    //assert(b >= 0 && b <= 10);  
61
    int i, result;  
62
    if (a == 0 || b == 0) {  
63
        //printf("branch 7\n");  
64
        result = 0;  
65
    } else {  
66
        //printf("branch 8\n");  
67
        result = a;  
68
        i = b;  
69
        while (i != 1) {  
70
            result = add(result, a);  
71
            i = i - 1;  
72
        }  
73
    }  
74
    return result;  
75
}  
76
  
77
int multiply_recursive(int a, int b) {  
78
    //assert(a >= -10 && a <= 10);  
79
    //assert(b >= 0 && b <= 10);  
80
    int result;  
81
  
82
    if (a == 0 || b == 0) {  
83
        //printf("branch 9\n");  
84
        result = 0;  
85
    } else {  
86
        if (b == 1) {  
87
           // printf("branch 10\n");  
88
            result = a;  
89
        } else {  
90
            //printf("branch 11\n");  
91
            result = add_recursive(a, multiply(a, b - 1));  
92
        }  
93
    }  
94
    return result;  
95
}  
96
  
97
int divide(int n, int m) {  
98
    //assert(n >= 0);  
99
    //assert(m > 0);  
100
    //assert(n <= 100 && m <= 100);  
101
  
102
    int q, r;  
103
  
104
    r = n;  
105
    q = 0;  
106
  
107
    while (r >= m) {  
108
        //printf("branch 12\n");  
109
        r = add(r, -m);  
110
        q = q + 1;  
111
    }  
112
  
113
    int result_1 = q;  
114
    int result_2 = r;  
115
	//{q, r};  
116
    return result_1;  
117
}  
118
  
119
int divide_recursive(int n, int m) {  
120
    //assert(n >= 0);  
121
    //assert(m > 0);  
122
    //assert(n <= 100 && m <= 100);  
123
  
124
    int result_quotient, result_remainder;  
125
	int res_remainder, res_quotient;  
126
  
127
    if (n < m) {  
128
        //printf("branch 13\n");  
129
        result_quotient = 0;  
130
        result_remainder = n;  
131
    } else {  
132
        //printf("branch 14\n");  
133
        res_quotient = divide_recursive(add_recursive(n, -m), m);  
134
        result_quotient = res_quotient + 1;  
135
        result_remainder = res_remainder;  
136
    }  
137
  
138
    return result_quotient;  
139
}  
140
  
141
// Main function for testing  
142
int main() {      
143
    // Test add  
144
    //printf("Add: %d\n", add(5, 3));  
145
      
146
    // Test add_recursive  
147
    //printf("Add recursive: %d\n", add_recursive(5, 3));  
148
      
149
    // Test multiply  
150
    //printf("Multiply: %d\n", multiply(5, 3));  
151
      
152
    // Test multiply_recursive  
153
    //printf("Multiply recursive: %d\n", multiply_recursive(5, 3));  
154
      
155
    // Test divide  
156
    //int div_result = divide(10, 3);  
157
    //printf("Divide: quotient = %d, remainder = %d\n", div_result.quotient, div_result.remainder);  
158
      
159
    // Test divide_recursive  
160
    //int div_result_rec = divide_recursive(10, 3);  
161
    //printf("Divide recursive: quotient = %d, remainder = %d\n", div_result_rec.quotient, div_result_rec.remainder);  
162
      
163
    int n, m;  
164
    int a, b;  
165
  
166
	add (a, b);  
167
	add_recursive (a, b);  
168
  
169
	multiply(a, b);  
170
	multiply_recursive(a, b);  
171
	  
172
    divide (n, m);  
173
	divide_recursive (n, m);  
174
	   
175
    return 0;  
176
}  
177
  
DateTimeLevelComponentMessage
2024-08-2120:22:47:018INFOCPAMain.detectFrontendLanguageIfNecessaryLanguage C detected and set for analysis
2024-08-2120:22:47:048INFOResourceLimitChecker.fromConfigurationUsing the following resource limits: CPU-time limit of 900s
2024-08-2120:22:47:111INFOCPAchecker.runCPAchecker 3.0 / testCaseGeneration-bmc (Java HotSpot(TM) 64-Bit Server VM 20.0.2) started
2024-08-2120:22:47:126INFOCPAchecker.parseParsing CFA from file(s) "doc/examples/arithmetic_2.c"
2024-08-2120:22:47:881INFOPredicateCPA
PredicateCPA.<init>
Using predicate analysis with MathSAT5 version 5.6.10 (953b604e7ca7) (May 31 2023 12:36:26, gmp 6.0.0/mpir 3.0.0, msvc 19.12, 64-bit).
2024-08-2120:22:48:191WARNINGCPAchecker.printConfigurationWarningsThe following configuration options were specified but are not used:
cpa.automaton.breakOnTargetState
2024-08-2120:22:48:191INFOCPAchecker.runAlgorithmStarting analysis ...
2024-08-2120:22:48:202INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:261INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:262INFOAbstractBMCAlgorithm.analyzeCounterexample0Error found, creating error path
2024-08-2120:22:48:295INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:297INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:298INFOAbstractBMCAlgorithm.analyzeCounterexample0Error found, creating error path
2024-08-2120:22:48:308INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:317INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:318INFOAbstractBMCAlgorithm.analyzeCounterexample0Error found, creating error path
2024-08-2120:22:48:327INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:329INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:330INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:48:331INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:337INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:338INFOAbstractBMCAlgorithm.analyzeCounterexample0Error found, creating error path
2024-08-2120:22:48:348INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:350INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:351INFOAbstractBMCAlgorithm.analyzeCounterexample0Error found, creating error path
2024-08-2120:22:48:360INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:373INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:373INFOAbstractBMCAlgorithm.analyzeCounterexample0Error found, creating error path
2024-08-2120:22:48:388INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:390INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:390INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:48:391INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:397INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:397INFOAbstractBMCAlgorithm.analyzeCounterexample0Error found, creating error path
2024-08-2120:22:48:408INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:409INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:410INFOAbstractBMCAlgorithm.analyzeCounterexample0Error found, creating error path
2024-08-2120:22:48:421INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:424INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:424INFOAbstractBMCAlgorithm.analyzeCounterexample0Error found, creating error path
2024-08-2120:22:48:435INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:440INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:440INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:48:442INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:446INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:448INFOAbstractBMCAlgorithm.analyzeCounterexample0Error found, creating error path
2024-08-2120:22:48:462INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:463INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:466INFOAbstractBMCAlgorithm.analyzeCounterexample0Error found, creating error path
2024-08-2120:22:48:480INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:484INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:486INFOAbstractBMCAlgorithm.analyzeCounterexample0Error found, creating error path
2024-08-2120:22:48:499INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:501INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:504INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:48:505INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:511INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:515INFOAbstractBMCAlgorithm.analyzeCounterexample0Error found, creating error path
2024-08-2120:22:48:531INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:533INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:537INFOAbstractBMCAlgorithm.analyzeCounterexample0Error found, creating error path
2024-08-2120:22:48:552INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:558INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:559INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:48:563INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 2
2024-08-2120:22:48:563INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:567INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:571INFOAbstractBMCAlgorithm.analyzeCounterexample0Error found, creating error path
2024-08-2120:22:48:585INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:616INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:620INFOAbstractBMCAlgorithm.analyzeCounterexample0Error found, creating error path
2024-08-2120:22:48:634INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:638INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:642INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:48:656INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 3
2024-08-2120:22:48:657INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:740INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:741INFOAbstractBMCAlgorithm.analyzeCounterexample0Error found, creating error path
2024-08-2120:22:48:749INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:755INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:756INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:48:781INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 4
2024-08-2120:22:48:782INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:806INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:807INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:48:831INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 5
2024-08-2120:22:48:832INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:852INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:854INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:48:879INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 6
2024-08-2120:22:48:880INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:900INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:901INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:48:928INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 7
2024-08-2120:22:48:928INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:48:949INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:48:951INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:48:981INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 8
2024-08-2120:22:48:982INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:49:002INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:49:003INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:49:035INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 9
2024-08-2120:22:49:036INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:49:053INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:49:054INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:49:091INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 10
2024-08-2120:22:49:092INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:49:108INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:49:109INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:49:145INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 11
2024-08-2120:22:49:145INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:49:163INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:49:164INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:49:200INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 12
2024-08-2120:22:49:201INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:49:217INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:49:219INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:49:260INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 13
2024-08-2120:22:49:261INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:49:276INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:49:278INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:49:317INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 14
2024-08-2120:22:49:317INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:49:336INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:49:338INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:49:391INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 15
2024-08-2120:22:49:391INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:49:407INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:49:409INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:49:449INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 16
2024-08-2120:22:49:450INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:49:465INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:49:466INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:49:508INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 17
2024-08-2120:22:49:509INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:49:524INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:49:526INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:49:572INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 18
2024-08-2120:22:49:573INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:49:587INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:49:589INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:49:636INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 19
2024-08-2120:22:49:637INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:49:653INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:49:656INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:49:708INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 20
2024-08-2120:22:49:708INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:49:726INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:49:728INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:49:784INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 21
2024-08-2120:22:49:784INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:49:807INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:49:809INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:49:884INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 22
2024-08-2120:22:49:884INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:49:899INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:49:902INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:49:953INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 23
2024-08-2120:22:49:954INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:49:968INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:49:970INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:50:034INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 24
2024-08-2120:22:50:035INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:50:050INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:50:052INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:50:109INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 25
2024-08-2120:22:50:109INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:50:125INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:50:127INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:50:180INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 26
2024-08-2120:22:50:181INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:50:194INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:50:197INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:50:258INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 27
2024-08-2120:22:50:258INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:50:277INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:50:280INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:50:342INFOLoopBoundCPA
LoopBoundPrecisionAdjustment.nextState
Adjusting maxLoopIterations to 28
2024-08-2120:22:50:342INFOAbstractBMCAlgorithm.runCreating formula for program
2024-08-2120:22:50:358INFOAbstractBMCAlgorithm.boundedModelCheckStarting satisfiability check...
2024-08-2120:22:50:361INFOAbstractBMCAlgorithm.checkBoundingAssertionsStarting assertions check...
2024-08-2120:22:50:405WARNINGForceTerminationOnShutdown$1.shutdownRequestedShutdown requested (The JVM is shutting down, probably because Ctrl+C was pressed.), waiting for termination.
2024-08-2120:22:50:448SEVERETestCaseGeneratorAlgorithm.run17 of 26 covered
2024-08-2120:22:50:448WARNINGShutdownNotifier.shutdownIfNecessaryWarning: Analysis interrupted (The JVM is shutting down, probably because Ctrl+C was pressed.)
Statistics NameStatistics ValueAdditional Value
PredicateCPA statistics
Number of abstractions 49 1% of all post computations
Times abstraction was reused 0
Because of function entry/exit 0 0%
Because of loop head 0 0%
Because of join nodes 0 0%
Because of threshold 0 0%
Because of target state 49 100%
Times precision was empty 49 100%
Times precision was {false} 0 0%
Times result was cached 0 0%
Times cartesian abs was used 0 0%
Times boolean abs was used 0 0%
Times result was 'false' 0 0%
Number of strengthen sat checks 0
Number of coverage checks 614
BDD entailment checks 0
Number of SMT sat checks 0
trivial 0
cached 0
Max ABE block size 46
Avg ABE block size 21.41 sum: 1049, count: 49, min: 8, max: 46
Number of predicates discovered 0
Time for post operator 0.236s
Time for path formula creation 0.232s
Time for strengthen operator 0.004s
Time for prec operator 0.013s
Time for abstraction 0.002s Max: 0.001s, Count: 49
Solving time 0.000s Max: 0.000s
Model enumeration time 0.000s
Time for BDD construction 0.000s Max: 0.000s
Time for merge operator 0.009s
Time for coverage checks 0.001s
Total time for SMT solver (w/o itp) 0.000s
Total number of created targets for pointer analysis 0
KeyValue statistics
Init. function predicates 0
Init. global predicates 0
Init. location predicates 0
Invariant Generation statistics
Bounds CPA statistics
Bound k 28
Maximum loop iteration reached 29
ValueAnalysisCPA statistics
Number of variables per state 1.23 sum: 6832, count: 5552, min: 0, max: 2
Number of global variables per state 0.00 sum: 0, count: 5552, min: 0, max: 0
Number of assumptions 1528
Number of deterministic assumptions 0
Level of Determinism 0%
ValueAnalysisPrecisionAdjustment statistics
Number of abstraction computations 6608
Total time for liveness abstraction 0.000s
Total time for abstraction computation 0.003s
Total time for path thresholds 0.000s
ConstraintsStrengthenOperator statistics
Total time for strengthening by ConstraintsCPA 0.000s
Replaced symbolic expressions 0
CPA algorithm statistics
Number of iterations 6614
Max size of waitlist 437
Average size of waitlist 219
LoopstackSortedWaitlist 43.48 sum: 6435, count: 148, min: 0, max: 233
ReversePostorderSortedWaitlist 20.07 sum: 5619, count: 280, min: 0, max: 170
LoopIterationSortedWaitlist 42.59 sum: 6303, count: 148, min: 0, max: 231
CallstackSortedWaitlist 1910.86 sum: 93632, count: 49, min: 0, max: 6466
Number of computed successors 6644
Max successors for one state 2
Number of times merged 290
Number of times stopped 297
Number of times breaked 49
Total time for CPA algorithm 0.558s Max: 0.083s
Time for choose from waitlist 0.008s
Time for precision adjustment 0.067s
Time for transfer relation 0.394s
Time for merge operator 0.025s
Time for stop operator 0.016s
Time for adding to reached set 0.012s
BMC algorithm statistics
Time for BMC formula creation 0.602s
Time for final sat check 0.041s
Time for error-path creation 0.020s
Time for error-path post-processing 0.165s
Time for bounding assertions check 1.147s
Testtargets statistics
Test target coverage 65.38%
Number of total original test targets 26
Number of total test targets 26
Number of covered test targets 17
Number of uncovered test targets 9
Total time for test goal reduction 0.000s
Code Coverage
Function coverage 1.000
Visited lines 49
Total lines 63
Line coverage 0.778
Visited conditions 17
Total conditions 26
Condition coverage 0.654
CPAchecker general statistics
Number of program locations 122
Number of CFA edges (per node) 142 count: 122, min: 0, max: 5, avg: 1.16
Number of relevant variables 29
Number of functions 7
Number of loops (and loop nodes) 4 sum: 16, min: 4, max: 4, avg: 4.00
Size of reached set 5552
Number of reached locations 93 76%
Avg states per location 59
Max states per location 685 at node N0
Number of reached functions 7 100%
Number of partitions 5539
Avg size of partitions 1
Max size of partitions 5 (with key [N86 (before line 110), Function divide called from node N119, stack depth 2 [b25b095], stack [main, divide], ABS0: true, Undetermined loop iteration state; at least 3 iterations in some loop ({Loop with heads [N10]
incoming [line 24: N9 -{while}-> N10]
outgoing [line 24: N10 -{[!i != 0]}-> N12]
nodes [N10, N11, N13, N14]
=3 through Loop with heads [N10]
incoming [line 24: N9 -{while}-> N10]
outgoing [line 24: N10 -{[!i != 0]}-> N12]
nodes [N10, N11, N13, N14]
, Loop with heads [N17]
incoming [line 32: N16 -{while}-> N17]
outgoing [line 32: N17 -{[!i != 0]}-> N19]
nodes [N17, N18, N20, N21]
=3 through Loop with heads [N17]
incoming [line 32: N16 -{while}-> N17]
outgoing [line 32: N17 -{[!i != 0]}-> N19]
nodes [N17, N18, N20, N21]
, Loop with heads [N83]
incoming [line 107: N82 -{while}-> N83]
outgoing [line 107: N83 -{[!r >= m]}-> N85]
nodes [N83, N84, N86, N87]
=3 through Loop with heads [N83]
incoming [line 107: N82 -{while}-> N83]
outgoing [line 107: N83 -{[!r >= m]}-> N85]
nodes [N83, N84, N86, N87]
})., stack depth 0 [2e0ad709]])
Number of target states 0
Size of final wait list 400
Time for analysis setup 1.065s
Time for loading CPAs 0.457s
Time for loading parser 0.136s
Time for CFA construction 0.423s
Time for parsing file(s) 0.197s
Time for AST to CFA 0.101s
Time for CFA sanity check 0.012s
Time for post-processing 0.082s
Time for loop structure 0.005s
Time for AST structure 0.000s
Time for CFA export 0.366s
Time for function pointers resolving 0.003s
Function calls via function pointers 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer calls 0 count: 1, min: 0, max: 0, avg: 0.00
Function calls with function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Time for classifying variables 0.050s
Time for collecting variables 0.022s
Time for solving dependencies 0.001s
Time for building hierarchy 0.000s
Time for building classification 0.018s
Time for exporting data 0.009s
Time for Analysis 2.256s
CPU time for analysis 1.078s
Total time for CPAchecker 3.322s
Total CPU time for CPAchecker 1.313s
Time for statistics 0.113s
Time for Garbage Collector 0.039s in 11 runs
Garbage Collector(s) used G1 Concurrent GC, G1 Old Generation, G1 Young Generation
Used heap memory 49MB ( 47 MiB) max; 30MB ( 29 MiB) avg; 57MB ( 54 MiB) peak
Used non-heap memory 53MB ( 50 MiB) max; 42MB ( 40 MiB) avg; 54MB ( 51 MiB) peak
Used in G1 Old Gen pool 18MB ( 17 MiB) max; 12MB ( 12 MiB) avg; 18MB ( 17 MiB) peak
Allocated heap memory 532MB ( 508 MiB) max; 181MB ( 173 MiB) avg
Allocated non-heap memory 53MB ( 51 MiB) max; 44MB ( 42 MiB) avg
Total process virtual memory 689MB ( 657 MiB) max; 394MB ( 376 MiB) avg
#Configuration NameConfiguration Value
1analysis.algorithm.BMC true
2analysis.entryFunction main
3analysis.name testCaseGeneration-bmc
4analysis.programNames doc/examples/arithmetic_2.c
5analysis.traversal.order bfs
6analysis.traversal.useCallstack true
7analysis.traversal.useReverseLoopIterationCount true
8analysis.traversal.useReverseLoopstack true
9analysis.traversal.useReversePostorder true
10analysis.useTestCaseGeneratorAlgorithm true
11ARGCPA.cpa cpa.composite.CompositeCPA
12CompositeCPA.cpas cpa.location.LocationCPA, cpa.callstack.CallstackCPA, cpa.functionpointer.FunctionPointerCPA, cpa.predicate.PredicateCPA, cpa.assumptions.storage.AssumptionStorageCPA, cpa.loopbound.LoopBoundCPA, cpa.value.ValueAnalysisCPA, cpa.testtargets.TestTargetCPA
13cpa cpa.arg.ARGCPA
14cpa.arg.lateMerge prevent
15cpa.automaton.breakOnTargetState 0
16cpa.composite.aggregateBasicBlocks false
17cpa.loopbound.maxLoopIterationAdjusterFactory INCREMENT
18cpa.loopbound.maxLoopIterations 1
19cpa.loopbound.maxLoopIterationsUpperBound 0
20cpa.predicate.blk.alwaysAtFunctions false
21cpa.predicate.blk.alwaysAtLoops false
22cpa.predicate.blk.useCache false
23cpa.predicate.ignoreIrrelevantVariables false
24cpa.predicate.invariants.export false
25cpa.predicate.invariants.exportAsPrecision false
26cpa.predicate.predmap.export false
27cpa.value.merge JOIN
28language C
29limits.time.cpu 900s
30log.level INFO
31specification config/properties/coverage-branches.prp
32testcase.targets.type TEST_COMP_ASSUME

About

This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.

License: Apache 2.0 License

This application includes third-party dependencies under different licenses. Click here to view them.

{{dependency.name}} {{dependency.version}}

Source: {{dependency.repository}}

{{dependency.copyright}}

License:

Full text of license
{{dependencies.licenses[dependency.licenseId]}}